Nuprl Lemma : equipollent_functionality_wrt_equipollent 11,40
A1, A2, B1, B2:Type.  A1 ~ A2   B1 ~ B2  ( A1 ~ B1   A2 ~ B2) 
latex

DefinitionsP  Q, x:A. B(x), t  T, Type,  A ~ B, P  Q, P & Q, P  Q
Lemmasequipollent wf, equipollent inversion, equipollent transitivity

origin